es:event_system{i:l}, L:(Id List), e:es-E(es).
f-msg{wanted:ut2, free:ut2, z:ut2}(es; L; e)  prop{i:l} 

latex

Definitions	False, P  Q, A  B, IdLnk, A, x:A. B(x), mkid{$x:ut2}, P  Q, A c B, (x  l), P  Q, f-msg{$wanted:ut2, $free:ut2, $z:ut2}(es; L; e), prop{i:l}, t  T, Id, x:A. B(x),
Lemmas	event system wf, es-E wf, es-lnk wf, false wf, es-tag wf, select wf, es-loc wf, Id wf, length wf1, nat wf